\begin{tabbing}
es{-}atom(${\it es}$;$i$;$a$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}trans(${\it es}$;$i$):$k$:Knd$\rightarrow$es{-}kindtype(${\it es}$;$i$;$k$)$\rightarrow$es{-}state(${\it es}$;$i$)$\rightarrow$es{-}state(${\it es}$;$i$)$>>$$a$\+
\\[0ex]$\vee$ es{-}send(${\it es}$;$i$):$k$:Knd$\rightarrow$es{-}kindtype(${\it es}$;$i$;$k$)$\rightarrow$es{-}state(${\it es}$;$i$)$\rightarrow$(es{-}Msg(${\it es}$) List)$>>$$a$
\\[0ex]$\vee$ es{-}choose(${\it es}$;$i$):$b$:Id$\rightarrow$es{-}state(${\it es}$;$i$)$\rightarrow$(es{-}kindtype(${\it es}$;$i$;locl($b$))+Unit)$>>$$a$
\-
\end{tabbing}